(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 15))
(declare-fun a1 () (Array  (_ BitVec 5)  (_ BitVec 11)))
(assert (let ((e2(_ bv3 2)))
(let ((e3 ((_ extract 7 2) v0)))
(let ((e4 (bvlshr ((_ zero_extend 13) e2) v0)))
(let ((e5 (store a1 ((_ extract 5 1) e3) ((_ sign_extend 9) e2))))
(let ((e6 (store e5 ((_ zero_extend 3) e2) ((_ extract 11 1) v0))))
(let ((e7 (select e6 ((_ extract 5 1) v0))))
(let ((e8 (store a1 ((_ extract 4 0) e3) ((_ zero_extend 5) e3))))
(let ((e9 (select e8 ((_ extract 5 1) e3))))
(let ((e10 (bvsub ((_ sign_extend 4) e9) v0)))
(let ((e11 (bvnor e7 e9)))
(let ((e12 (bvmul ((_ zero_extend 4) e9) e10)))
(let ((e13 (bvadd e12 e4)))
(let ((e14 (bvsdiv ((_ sign_extend 9) e2) e7)))
(let ((e15 ((_ rotate_left 5) e3)))
(let ((e16 (= e4 ((_ zero_extend 4) e7))))
(let ((e17 (bvsgt e9 e14)))
(let ((e18 (bvsgt e11 e14)))
(let ((e19 (bvugt ((_ zero_extend 5) e3) e11)))
(let ((e20 (bvsle e12 ((_ sign_extend 9) e15))))
(let ((e21 (bvule ((_ sign_extend 5) e3) e14)))
(let ((e22 (distinct e10 ((_ zero_extend 13) e2))))
(let ((e23 (= e4 e4)))
(let ((e24 (bvsle e11 ((_ zero_extend 5) e15))))
(let ((e25 (bvuge e13 ((_ zero_extend 9) e15))))
(let ((e26 (distinct ((_ sign_extend 4) e9) v0)))
(let ((e27 (= e16 e24)))
(let ((e28 (and e25 e20)))
(let ((e29 (=> e23 e21)))
(let ((e30 (not e18)))
(let ((e31 (=> e17 e17)))
(let ((e32 (or e26 e27)))
(let ((e33 (ite e19 e22 e30)))
(let ((e34 (and e29 e28)))
(let ((e35 (or e31 e33)))
(let ((e36 (or e32 e34)))
(let ((e37 (xor e36 e35)))
(let ((e38 (and e37 (not (= e7 (_ bv0 11))))))
(let ((e39 (and e38 (not (= e7 (bvnot (_ bv0 11)))))))
e39
)))))))))))))))))))))))))))))))))))))))

(check-sat)
